functor Ir (S : IR_STRUCTS) : IR =
struct
  open S
  
  structure T = Types 
  structure Id = Id
  
  type id = Id.t
  type pos = int
  
  structure Binop =
  struct
    datatype t
      = Plus
      | Minus
      | Times
      | Divide
      | Modus
      | And
      | Or
      | Eq
      | Ne
      | Gt
      | Ge
      | Lt
      | Le
    
    fun equals (x1, x2) = x1 = x2
    
    fun toString x =
        case x
         of Plus => " + "
          | Minus => " - "
          | Times => " * "
          | Divide => " / "
          | Modus => " % "
          | And => " && "
          | Or => " || "
          | Eq => " == "
          | Ne => " != "
          | Gt => " > "
          | Ge => " >= "
          | Lt => " < "
          | Le => " <= "
  end

  structure Le =
  struct
    datatype exp
      = Expvoid
      | IntNum of Intl.t
      | True
      | False
      | Null
      | Lval of {lval : lval, ty : Types.t}
      | BinopExp of {left : exp, bop : Binop.t, right : exp, ty : Types.t, pos : pos}
      | NotExp of exp * pos
      | Result
      | Imply of exp * exp * pos
      | Iff of exp * exp * pos
      | Forall of Id.t * Types.t * exp * pos
      | Exists of Id.t * Types.t * exp * pos
      | Pi of lval list list * pos
      | N of lval list * pos
      | D of lval list * pos
      | Prev of lval * pos
      | LList of exp * pos
      | Tree of exp * pos
      | Pred of Id.t * exp * pos
      | Let of exp * exp * exp * pos

    and lval
      = Var of {id : Id.t, ty : Types.t, pos: pos}
      | Ptr of lval * lval * pos
      | Sharp of Types.t
      | Inarray of {lval : lval, exp : exp, length : Intl.t, ty : Types.t, pos : pos}
      | Instruct of {lval : lval, id : Id.t, offSet : Intl.t, pos : pos}
      | Instruct2 of lval * Id.t * Id.t * pos
      | Upd of lval * exp * exp
      | Sel of lval * exp

    fun equalsExp (x1,x2)= 
        case (x1, x2)
         of (Expvoid, Expvoid) => true
          | (IntNum i1, IntNum i2) => Intl.equals (i1, i2)
          | (True, True) => true
          | (False, False) => true
          | (Null, Null) => true
          | (Lval {lval=l1, ty=ty1}, Lval {lval=l2, ty=ty2} ) => 
                equalsLval (l1, l2) andalso T.equals (ty1,ty2)
          | (BinopExp {left=e1, bop=b1, right=e2, ty=ty1, pos=pos1}, 
             BinopExp {left=e3, bop=b2, right=e4, ty=ty2, pos=pos2} ) =>
                (pos1=pos2) andalso equalsExp (e1,e3) 
                andalso Binop.equals (b1,b2) andalso equalsExp (e2,e4)
                andalso T.equals (ty1, ty2)
          | (NotExp (e1, pos1), NotExp (e2, pos2)) =>
                equalsExp (e1, e2)
                andalso (pos1 = pos2)
          | (Result, Result) => true
          | (Imply (e1, e2, pos1), Imply (e3, e4, pos2)) =>
                equalsExp (e1, e3)
                andalso equalsExp (e2, e4)
                andalso (pos1 = pos2)
          | (Forall (id1, t1, e1, pos1), Forall (id2, t2, e2, pos2)) =>
                Id.equals (id1, id2)
                andalso T.equals (t1, t2)
                andalso equalsExp (e1, e2)
                andalso (pos1 = pos2)
          | (Exists (id1, t1, e1, pos1), Exists (id2, t2, e2, pos2)) =>
                Id.equals (id1, id2)
                andalso T.equals (t1, t2)
                andalso equalsExp (e1, e2)
                andalso (pos1 = pos2)
          | (Pi (lvalss1, pos1), Pi (lvalss2, pos2)) =>
                equalsLvalss (lvalss1, lvalss2)
                andalso (pos1 = pos2)
          | (N (lvals1, pos1), N (lvals2, pos2)) =>
                equalsLvals (lvals1, lvals2)
                andalso (pos1 = pos2)
          | (D (lvals1, pos1), D (lvals2, pos2)) =>
                equalsLvals (lvals1, lvals2)
                andalso (pos1 = pos2)
          | (Prev (lval1, pos1), Prev (lval2, pos2)) =>
                equalsLval (lval1, lval2)
                andalso (pos1 = pos2)
          | (LList (e1, pos1), LList (e2, pos2)) =>
                equalsExp (e1, e2)
                andalso (pos1 = pos2)
          | (Tree (e1, pos1), Tree (e2, pos2)) =>
                equalsExp (e1, e2)
                andalso (pos1 = pos2)
          | (Pred (id1, e1, pos1), Pred (id2, e2, pos2)) =>
                Id.equals (id1, id2)
                andalso equalsExp (e1, e2)
                andalso (pos1 = pos2)
          | (Let (e1, e2, e3, pos1), Let (e4, e5, e6, pos2)) =>
                equalsExp (e1, e4)
                andalso equalsExp (e2, e5)
                andalso equalsExp (e3, e6)
                andalso (pos1 = pos2)
          | _ => false
          
    and equalsLval  (x1, x2) =
        case (x1, x2)
         of (Var {id=id1, ty=ty1, pos=pos1}, 
             Var {id=id2, ty=ty2, pos=pos2} )  => 
                (pos1=pos2) andalso Id.equals (id1,id2) andalso T.equals (ty1,ty2)
          | (Ptr (lv1,lv11,pos1), Ptr (lv2,lv22,pos2)) => 
                (pos1=pos2) andalso equalsLval(lv1,lv2) andalso equalsLval (lv11,lv22)
          | (Sharp s1, Sharp s2) => T.equals (s1,s2)
          | (Inarray {lval=lv1,exp=exp1,length=len1,ty=ty1,pos=pos1}, 
             Inarray {lval=lv2,exp=exp2,length=len2,ty=ty2,pos=pos2} )=>
                (pos1=pos2) 
                andalso equalsLval(lv1,lv2)
                andalso equalsExp(exp1,exp2)
                andalso Intl.equals (len1,len2)
                andalso T.equals (ty1, ty2)
          | (Instruct {lval = lv1, id = id1, offSet = offSet1, pos = pos1},
             Instruct {lval = lv2, id = id2, offSet = offSet2, pos = pos2}) =>
                (pos1=pos2)
                andalso equalsLval(lv1,lv2)
                andalso Id.equals(id1,id2)
          | (Instruct2 (lv1,id1,id11,pos1), Instruct2 (lv2,id2,id22,pos2)) =>
                (pos1=pos2)
                andalso equalsLval(lv1,lv2)
                andalso Id.equals(id1,id2)
                andalso Id.equals(id11,id22)
          | (Upd (lv1,exp1a,exp2a), Upd (lv2,exp1b,exp2b)) =>
                equalsLval(lv1,lv2)
          		andalso equalsExp(exp1a,exp1b)
          		andalso equalsExp(exp2a,exp2b)
          | (Sel (lv1,exp1), Sel (lv2,exp2)) =>
                equalsLval(lv1,lv2)
          		andalso equalsExp(exp1,exp2)
          | _ => false
    and equalsLvals (l1, l2) =
        case (l1, l2)
         of ([], []) => true
          | (x :: xs, y :: ys) => equalsLval (x, y) andalso equalsLvals (xs, ys)
          | _ => false
         
    and equalsLvalss (ls1, ls2) =
        case (ls1, ls2)
         of ([], []) => true
          | (x :: xs, y :: ys) => equalsLvals (x, y) andalso equalsLvalss (xs, ys)
          | _ => false 
    
    fun equalsExps (l1,l2) =
        case (l1,l2)
          of ([],[]) => true
           | (x::xs, y::ys) => equalsExp (x,y) andalso equalsExps (xs,ys)
           | _ => false
           
    fun expToString x =
        case x
         of Expvoid => "void"
 	        | IntNum i => Intl.toString i
	        | True => "true"
	        | False => "false"
	        | Null => "Null"
	        | Lval {lval,ty} => lvalToString lval
	        | BinopExp {left,bop,right,ty,pos} => "("^(expToString left)^")"^(Binop.toString bop)^"("^(expToString right)^")"
	        | NotExp(e, p) => "!("^(expToString e)^")"
	        | Result => "result" 
	        | Imply(e1, e2, p) => "("^(expToString e1)^(") => (")^(expToString e2)^")"
					| Iff (e1, e2, pos) => 
	          String.concat ["(", expToString e1, ")", "<=>", "(", expToString e2, ")"]
	        | Forall (id, ty, e, pos) =>
	          String.concat ["forall ", Id.toString id, ":", T.toString ty, "(", expToString e, ")"]
	        | Exists (id, ty, e, pos) =>
	          String.concat ["exists ", Id.toString id, ":", T.toString ty, "(", expToString e, ")"]
	        | Pi (lss, pos) => "" 
	        | N (ls, pos) => ""    
	        | D (ls, pos) => ""
	        | Prev (lval, pos) => String.concat ["prev(", lvalToString lval, ")"]
	        | LList (exp, pos) => String.concat ["list(", expToString exp, ")"]
	        | Tree (exp, pos) => String.concat ["tree(", expToString exp, ")"]
	        | Pred (id, exp, pos) => String.concat [Id.toString id, "(", expToString exp, ")"]
	        | Let (e1, e2, e3, pos) => 
	          String.concat ["let ", expToString e1, " = ", expToString e2, " in ", expToString e3, " end"]
			and lvalToString lval = 
	      case lval
	       of Var {id, ty, pos} => Id.toString id
	        | Ptr (lval1, lval2, pos) => String.concat ["(", lvalToString lval1, ")->", lvalToString lval2]
	        | Sharp ty => String.concat ["#", T.toString ty]
	        | Inarray {lval, exp, length, ty, pos} => String.concat [lvalToString lval, "[", expToString exp, "]"]
	        | Instruct {lval = lval1, id, offSet, pos} =>
	          String.concat [lvalToString lval1, ".", Id.toString id]
	        | Instruct2 (lval1, id1, id2, pos) => String.concat [lvalToString lval1, ".", Id.toString id1, ".", Id.toString id2]
					| Upd (lval,exp1,exp2) => String.concat ["upd(", lvalToString lval, ", ", expToString exp1, ", ", expToString exp2, ")"]
					| Sel (lval,exp) => String.concat ["sel(", lvalToString lval, ", ", expToString exp, ")"]
			fun expsToString es =
	     case es
	       of [] => ""
	        | [e] => expToString e
	        | x :: xs => String.concat [expToString x, ", ", expsToString xs]
	        
	    fun ppProp e = String.concat ["/*@ ", expToString e,  " */"]
	    fun space n =
      case n
       of 0 => ""
        | i => String.concat [" ", space (i - 1)]
  end
  
  structure Stm =
  struct
    datatype t
      = AsnExp of {lval : Le.lval, exp : Le.exp, ty : Types.t, pos : pos}
      | AsnAlloc of {lval : Le.lval, ty : Types.t, pos : pos}
      | AsnCall of {lval : Le.lval, fid : Id.t, ty : Types.t, exps : Le.exp list, pos : pos}
      | If of Le.exp * t list * t list * pos
      | While of {condition : Le.exp, invariant : Le.exp, body : t list, pos : pos}
      | Return of {exp : Le.exp, fty : Types.t, pos : pos}
      | Call of Id.t * (Le.exp list) * pos
      | Free of Le.exp * pos
      | Prop of Le.exp * pos

    val bogus = fn _ => raise Fail "bogus"
    
    fun endWithReturn s =
        case s
         of AsnExp {lval,exp,ty,pos} => false
          | AsnAlloc {lval, ty, pos} => false
          | AsnCall {lval, fid, ty, exps, pos} => false
          | If (e, s1, s2, pos) => endWithReturns s1 andalso endWithReturns s2
          | While {invariant, condition, body, pos} => false
          | Return {exp, fty, pos} => true
          | Call (fid, es, pos) => false
          | Free (e, pos) => false
          | Prop (e, pos) => false
    and endWithReturns ss =
        case ss
         of [] => false
          | x :: xs =>
            if endWithReturn x
            then true
            else endWithReturns xs
          
    fun ppStm (sp, stm) =
      case stm 
       of AsnExp {lval,exp,ty,pos} =>
          String.concat [Le.space sp, Le.lvalToString lval, "=", Le.expToString exp, ";"]
        | AsnAlloc {lval, ty, pos} =>
          String.concat [Le.space sp, Le.lvalToString lval, " = alloc (", T.toString ty, ")", ";"]
        | AsnCall {lval, fid, ty, exps, pos} =>
          String.concat [Le.space sp, Le.lvalToString lval, "=", Id.toString fid, "(", Le.expsToString exps, ")", ";"]
        | If (e, s1, s2, pos) =>
          String.concat [Le.space sp, "if (", Le.expToString e, ")\n",
                         Le.space sp, "{\n",
                         ppStms (sp+2, s1),
          		 Le.space sp, "}\n",
                         Le.space sp, "else\n",
                         Le.space sp, "{\n",
                         ppStms (sp+2, s2),
                         Le.space sp, "}"]
        | While {invariant, condition, body, pos} =>
          String.concat [Le.space sp, "while (", Le.expToString condition, ")", "    ", Le.ppProp invariant, "\n",
          		Le.space sp, "{\n",
          		ppStms (sp+2, body),
          		Le.space sp, "}"]
        | Return {exp, fty, pos} =>
          String.concat [Le.space sp, (*T.toString fty,*) "return ", Le.expToString exp, ";"]
        | Call (id, es, pos) =>
          String.concat [Le.space sp, Id.toString id, "(", Le.expsToString es, ")", ";"]
        | Free (e, pos) =>
          String.concat [Le.space sp, "free(", Le.expToString e, ")", ";"]
        | Prop (e, pos) =>
          String.concat [Le.space sp, Le.ppProp e, ";"] 
          
    and ppStms (sp, stms) = 
        String.concat (List.map (fn x => String.concat [ppStm (sp, x), "\n"]) stms)
        
    fun toString stm = ppStm (2, stm)
    fun toStringS stms = ppStms (2, stms)
    
    structure Map =
    BinaryMapFn (struct
                   type ord_key = Id.t
                   val compare = Id.compare
                 end)
         
    val mapRef : int Map.map ref = ref Map.empty
    
    fun look x =
        case Map.find (!mapRef, x)
         of NONE => 0
          | SOME x => x
    
    fun enter (x, v) = mapRef := Map.insert (!mapRef, x, v)
    
    fun numCallsStm s =
        case s
         of AsnExp {lval,exp,ty,pos} => ()
          | AsnAlloc {lval, ty, pos} => ()
          | AsnCall {lval, fid, ty, exps, pos} =>
            let val orig = look fid
                val _ = enter (fid, orig + 1)
            in  ()
            end
          | If (e, s1, s2, pos) =>
            let val _ = List.app numCallsStm s1
                val _ = List.app numCallsStm s2
            in  ()
            end
          | While {invariant, condition, body, pos} =>
            let val _ = List.app numCallsStm body
            in  ()
            end
          | Return {exp, fty, pos} => ()
          | Call (fid, es, pos) =>
            let val orig = look fid
                val _ = enter (fid, orig + 1)
            in  ()
            end
          | Free (e, pos) => ()
          | Prop (e, pos) => ()
        
    fun numCalls ss =
        let val _ = mapRef := Map.empty
            val _ = List.app numCallsStm ss
        in  Map.listItemsi (!mapRef)
        end    
  end

  structure Structs =
  struct
    datatype t
      = T of {name : Id.t,
              fields : {id : Id.t, ty : Types.t} list,
              pos : pos}
    
    fun bogus () = T {name = Id.bogus (), fields = [], pos = ~1}
    fun equals (s1, s2) = 
    	(*case (s1,s2)
    		of (T {name=n1, fields=fld1, pos=pos1},
    			  T {name=n2, fields=fld2, pos=pos2} ) =>
    			  (pos1=pos2)
    			  andalso Id.equals (n1,n2)
    			  andalso *)raise Fail "bogus"
    fun toString s= 
    	let fun listField fields = 
        case fields
          of [] => ""
           | {id,ty}::flds => 
                String.concat ["\n\t",T.toString ty," ",Id.toString id,";",listField flds]
      in 
        case s
          of T {name,fields,pos} => String.concat ["struct ",Id.toString name,"{",listField fields,"\n}"]
      end
  end

  structure Function =
  struct
    datatype t
      = T of {name : Id.t,
              rettype : Types.t,
              args : {id : Id.t, ty : Types.t} list,
              locals : {id : Id.t, ty : Types.t} list,
              stm : Stm.t list,
              pre : Le.exp,
              post : Le.exp,
              pos : pos}
    
    fun ppArgs args =
      case args
       of [] => ""
        | [{id, ty}] => String.concat [T.toString ty, " ", Id.toString id]
        | {id, ty} :: xs => String.concat [T.toString ty, " ", Id.toString id, ", ", ppArgs xs]
  
    fun ppOneLocal ({id, ty}) = String.concat ["  ", T.toString ty, " ", Id.toString id, ";\n"]
  
    fun ppLocals locals = String.concat (List.map ppOneLocal locals)
    
    fun name (T {name, ...}) = name 
    
    fun toString f =
      case f
       of T {name,
               rettype,
               args,
               locals,
               stm,
               pre,
               post,
               pos} =>
          String.concat [Le.ppProp pre, "\n",
                         T.toString rettype, " ", Id.toString name, "(", ppArgs args, ")\n",
                         "{\n",
                         ppLocals locals,
                         "\n\n",
                         Stm.toStringS stm,
                         "}\n",
                         Le.ppProp post, "\n\n\n"]
  end

  structure Program =
  struct
    datatype t
      = T of {structs : Structs.t list,
              gvars : {id : Id.t, ty : Types.t} list,
              funcs : Function.t list,
              pos : pos}

    val bogus = fn _ => raise Fail "bogus"
    
    fun ppGvars gvars = 
        let fun printvars {id,ty} = 
                String.concat ["\n", T.toString ty, " ", Id.toString id, ";"]
        in String.concat (List.map printvars gvars)
        end
        
     fun toString (T {structs,
                      gvars,
                      funcs, ...} ) : string =
          String.concat [String.concat (List.map Structs.toString structs),
                         ppGvars gvars, 
                         String.concat (List.map Function.toString funcs)]
  end
    
  (*    
  fun ptr2str (Lval(lval)) = lval2str lval
    | ptr2str _ = (print "not impl in ptir: 91:\n"; "")
  and lval2str lval = "\""^(lval2str1 lval)^"\""
  and lval2str1 lval =
      case lval
        of Var(id, pos) => Id.toString id
         | Ptr(lval1, lval2, pos) => "*"^(lval2str1 lval2)
         | Sharp(ty) => ""
         | Inarray(lval, e, sz, pos) => (lval2str1 lval)^"[...]"
         | Instruct(Ptr(lval1, lval2, pos1), id, pos2) => String.concat [lval2str1 lval2, "->", Id.toString id]
         | Instruct(lval, id, pos) => String.concat [lval2str1 lval, ".", Id.toString id]
         |  _ => (print "not in ptir: 98\n"; "")
  
  (**)
  fun pind2prop exdec =
      case exdec
        of ExdecSkip => ExdecSkip
         | ExdecSeq(exd1, exd2, pos) => ExdecSeq(pind2prop exd1, pind2prop exd2, pos)
         | ExdecStruct (id, idtylist, pos) => ExdecStruct (id, idtylist, pos)
         | ExdecVar(idtylist, pos) => ExdecVar(idtylist, pos)
         | ExdecFunc(id, ty, idtylist, idtylist2, stm, e1, e2, pos) =>
             ExdecFunc(id, ty, idtylist, idtylist2, stm2prop stm, exp2prop e1, exp2prop e2, pos)
  and stm2prop stm =
      case stm
        of Skip => Skip
         | AsnExp (lval, exp, tty, pos) => AsnExp (lval2prop lval, exp2prop exp, tty, pos)
         | AsnAlloc (lval, tty, bty, pos) => AsnAlloc (lval2prop lval, tty, bty, pos)
         | AsnCall (lval, id, es, tty, pos) => AsnCall (lval2prop lval, id, es2prop es, tty, pos)
         | Seq (s1, s2, pos) => Seq (stm2prop s1, stm2prop s2, pos)
         | If (e, s1, s2, pos) => If (exp2prop e, stm2prop s1, stm2prop s2, pos)
         | While (e1, e2, s, pos) => While (exp2prop e1, exp2prop e2, stm2prop s, pos)
         | Return (e, pos) => Return (exp2prop e, pos)
         | Call (id, es, pos) => Call (id, es2prop es, pos)
         | Free (e, pos) => Free (exp2prop e, pos)
         | Prop (e, pos) => Prop (exp2prop e, pos)
  and exp2prop exp =
      case exp
        of Expvoid => Expvoid
         | IntNum i => IntNum i
         | True => True
         | False => False
         | Null => Null
         | Lval lval => Lval (lval2prop lval)
         | BinopExp (e1, bop, e2, pos) => BinopExp(exp2prop e1, bop, exp2prop e2, pos)
         | Not(e, pos) => Not (exp2prop e, pos)
         | Result => Result
         | Imply (e1, e2, pos) => Imply (exp2prop e1, exp2prop e2, pos)
         | Forall (id, ty, e, pos) => Forall (id, ty, exp2prop e, pos)
         | Exists (id, ty, e, pos) => Exists (id, ty, exp2prop e, pos)
         | Pi (lvalss, pos) => trPi (lvalss, pos)
         | N (lvals, pos) => trN (lvals, pos)
         | D (lvals, pos) => trD (lvals, pos)
         | Prev (lval, pos) => Prev (lval2prop lval, pos)
         | LList (exp, pos) => LList (exp2prop exp, pos)
         | Tree (exp, pos) => Tree (exp2prop exp, pos)
         | Pred (id, e, pos) => Pred (id, exp2prop e, pos)
         | Let (e1, e2, e3, pos) => Let (exp2prop e1, exp2prop e2, exp2prop e3, pos)
  and lval2prop lval =
      case lval
        of Var (id, pos) => Var (id, pos)
         | Ptr (lval1, lval2, pos) => Ptr (lval2prop lval1, lval2prop lval2, pos)
         | Sharp mytype => Sharp mytype
         | Inarray (lval, exp, size, pos) => Inarray (lval2prop lval, exp2prop exp, size, pos)
         | Instruct (lval, id, pos) => Instruct (lval2prop lval, id, pos)
         | Instruct2 (lval, id1, id2, pos) => Instruct2 (lval2prop lval, id1, id2, pos)
         | Upd (lval, exp1, exp2) => Upd (lval2prop lval, exp2prop exp1, exp2prop exp2)
         | Sel (lval, exp) => Sel (lval2prop lval, exp2prop exp)
  and es2prop es = List.map exp2prop es
  and trPi (lvalss, pos) =
      let fun mklist l = (List.map (List.hd) l) handle Empty => raise Fail "compiler bug\n"
          fun make (x1, x2, pos) = 
              case x2
                of [] => raise Fail "compiler bug"
                 | [y] => BinopExp(Lval(x1), Binop.Ne, Lval(y), pos)
                 | y::ys =>
                     let val new = BinopExp(Lval(x1), Binop.Ne, Lval(y), pos)
                     in  BinopExp(new, Binop.And, make (x1, ys, pos), pos)
                     end
          fun h l = 
              case l
                of [] => raise Fail "compiler bug"
                 | [x] => raise Fail "compiler bug"
                 | x1::x2::[] => BinopExp(Lval(x1), Binop.Ne, Lval(x2), pos)
                 | x1::xs =>
                     let val new_e = make (x1, xs, pos)
                     in  BinopExp(new_e, Binop.And, (h xs), pos)
                     end
          fun g l = 
              case l
               of [] => raise Fail "compiler bug"
                | [x] => trPiHelp (x, pos)
                | x::xs =>
                    let val new_list = trPiHelp (x, pos)
                    in  BinopExp(new_list, Binop.And, trPi (xs, pos), pos)
                    end
      in  if List.length lvalss <= 1
          then g lvalss
          else BinopExp(g lvalss, Binop.And, h (mklist lvalss), pos)
      end
  and trPiHelp (l, pos) =
      let fun make (x1, x2, pos) = 
              case x2
                of [] => raise Fail "compiler bug"
                 | [y] => BinopExp(Lval(x1), Binop.Eq, Lval(y), pos)
                 | (y::ys) => 
                     let val new = BinopExp(Lval(x1), Binop.Eq, Lval(y), pos)
                     in  BinopExp(new, Binop.And, make (x1, ys, pos), pos)
                     end
      in  case l
            of [] => raise Fail "compiler bug"
             | [x] => BinopExp(Lval(x), Binop.Ne, Null, pos)
             | x::xs =>
               let val new = BinopExp(Lval(x), Binop.Ne, Null, pos)               
               in  BinopExp(new, Binop.And, make(x, xs, pos), pos)
               end
      end
  and trN (lvals, pos) =
      case lvals
        of [] => raise Fail "compiler bug"
         | [x] => BinopExp(Lval (x), Binop.Eq, Null, pos)
         | x :: xs =>
             let val new = BinopExp(Lval(x), Binop.Eq, Null, pos)
             in  BinopExp(new, Binop.And, trN (xs, pos), pos)
             end              
  and trD (lvals, pos) = trN (lvals, pos)
  
  fun selectB b = b  

  fun selectE e =
      case e
       of Expvoid => Expvoid
        | IntNum i => IntNum i
        | True => True
        | False => False
        | Null => Null
        | Lval lval => Lval(selectL lval)
        | BinopExp (e1, b, e2, p) => BinopExp(selectE e1, b, selectE e2, p)
        | Not (e, p) => Not(selectE e,p)
        | Result => Result
        | Imply (e1, e2, p) => Imply(selectE e1, selectE e2, p)
        | Forall (tid, ty, e1, p) => Forall(tid, ty, selectE e1, p)
        | Exists (tid, ty, e1, pos) => Exists(tid, ty, selectE e1, pos)
        | LList (exp, pos) => LList(selectE exp, pos)
        | Tree (exp, pos) => Tree(selectE exp, pos)
        | Pred (id, e, pos) => Pred(id, selectE e, pos)
        | Let (e1, e2, e3, pos) => Let(selectE e1, selectE e2, selectE e3, pos)
        | _ => raise Fail "not implemented yet\n" 
      
  and selectL lval =
      case lval
       of Var (id, pos) => Var (id, pos)
        | Ptr (Sharp ty,  lval, pos) => Sel (Sharp(ty), Lval(selectL lval))
        | Ptr (_, _, _) => raise Fail "fail in selectize...ptr\n"
        | Sharp _ => raise Fail "fail in selectize...sharp\n"
        | Inarray (lval, e, size,pos) => Sel (selectL lval, selectE e)
        | Instruct (lval, id, pos) => Sel (selectL lval, Lval(Var(id, pos)))
        | Instruct2 (lval, id1, id2, pos) => Sel (selectL lval, Lval (Var (Id.fromString "mayBeWrong", pos)))
        | Sel (lval, e) => raise Fail "fail in selectize...sel1\n"
        | Upd (l, e1, e2) => raise Fail "fail in selectize...upd\n"
  
  and selectEs es = List.map selectE es
  *)
end
